\begin{tabbing}
$\forall$${\it ds}$:top, ${\it da}$:fpf(Knd; $k$.Type), $x$,$T$:top, ${\it ks}$:(Knd List), ${\it tr}$:top, $j$,$i$:Id.
\\[0ex]R{-}da(R{-}state{-}var($i$; ${\it ds}$; ${\it da}$; $x$; $T$; ${\it ks}$; ${\it tr}$); $j$)
\\[0ex]=
\\[0ex]if eq\_id($i$; $j$)
\\[0ex]then reduce(\=($\lambda$$k$,$d_{1}$. fpf{-}join(Kind{-}deq; fpf{-}single($k$; ma{-}valtype(${\it da}$; $k$)); $d_{1}$));\+
\\[0ex]fpf{-}empty;
\\[0ex]${\it ks}$)
\-\\[0ex]else fpf{-}empty
\\[0ex]fi 
\\[0ex]$\in$ fpf(Knd; $k$.Type)
\end{tabbing}